The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
satck/0

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
member, eq, choice, guess, verify

They will be analysed ascendingly in the following order:
eq < member
member < verify
choice < guess

(8) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
eq, member, choice, guess, verify

They will be analysed ascendingly in the following order:
eq < member
member < verify
choice < guess

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol eq.

(10) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
member, choice, guess, verify

They will be analysed ascendingly in the following order:
member < verify
choice < guess

(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

Induction Base:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n127_2, 1)))) →_R^Ω(1)
if(eq(gen_true:false:nil:cons:O:0:1:unsat2_2(a), true), true, member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2)))) →_IH
if(eq(gen_true:false:nil:cons:O:0:1:unsat2_2(a), true), true, *3_2)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(12) Complex Obligation (BEST)

(13) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
choice, guess, verify

They will be analysed ascendingly in the following order:
choice < guess

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) → *3_2, rt ∈ Ω(n131898₂)

Induction Base:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n131898_2, 1)))) →_R^Ω(1)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) →_IH
*3_2

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(15) Complex Obligation (BEST)

(16) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) → *3_2, rt ∈ Ω(n131898₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
guess, verify

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132426_2))) → *3_2, rt ∈ Ω(n132426₂)

Induction Base:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n132426_2, 1)))) →_R^Ω(1)
cons(choice(true), guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132426_2)))) →_IH
cons(choice(true), *3_2)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(18) Complex Obligation (BEST)

(19) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) → *3_2, rt ∈ Ω(n131898₂)
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132426_2))) → *3_2, rt ∈ Ω(n132426₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
verify

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol verify.

(21) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) → *3_2, rt ∈ Ω(n131898₂)
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132426_2))) → *3_2, rt ∈ Ω(n132426₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(22) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(23) BOUNDS(n^1, INF)

(24) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) → *3_2, rt ∈ Ω(n131898₂)
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132426_2))) → *3_2, rt ∈ Ω(n132426₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(25) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(26) BOUNDS(n^1, INF)

(27) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131898_2))) → *3_2, rt ∈ Ω(n131898₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(28) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(29) BOUNDS(n^1, INF)

(30) Obligation:

Innermost TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(32) BOUNDS(n^1, INF)